package br.ufrn.btest.tests.unit;

import static org.junit.Assert.assertEquals;

import java.io.File;
import java.util.HashSet;
import java.util.Set;

import org.junit.Test;

import br.ufrn.btest.Partitioner;
import br.ufrn.btest.parser.Machine;
import br.ufrn.btest.parser.Operation;
import de.be4.classicalb.core.parser.BException;


public class PartitionerTest {

	
	@Test
	public void shouldGetInputSpaceVariables() {
		Machine machine = getMachineInstance("machines/Test.mch");
		
		Partitioner partitioner = new Partitioner(machine.getOperation(0));
		
		Set<String> expectedVariables = new HashSet<String>();
		expectedVariables.add("pressed");
		expectedVariables.add("foo");
		expectedVariables.add("test_variable");
		expectedVariables.add("test_variable3");
		expectedVariables.add("test_variable2");
		
		assertEquals(expectedVariables, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetInputSpaceForMachineWithoutInvariant() {
		Machine machine = getMachineInstance("machines/SimpleMachine.mch");
		
		Partitioner partitioner = new Partitioner(machine.getOperation(0));
		
		Set<String> expectedVariables = new HashSet<String>();
		expectedVariables.add("yy");
		expectedVariables.add("xx");
		
		assertEquals(expectedVariables, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetInputSpaceForMachineStructuredWithIncludes() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Locks.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedInputSpace = new HashSet<String>();
		expectedInputSpace.add("dd");
		expectedInputSpace.add("status");
		expectedInputSpace.add("position");
		
		assertEquals(expectedInputSpace, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetInputSpaceFromPromotedOperations() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Locks.mch");
		Operation operationUnderTest = machine.getOperation(3);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedInputSpace = new HashSet<String>();
		expectedInputSpace.add("dd");
		
		assertEquals(expectedInputSpace, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetInputSpaceForMachineStructuredWithSees() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Costumer.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedInputSpace = new HashSet<String>();
		expectedInputSpace.add("gg");
		expectedInputSpace.add("price");
		expectedInputSpace.add("limit");
		
		assertEquals(expectedInputSpace, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetInputSpaceForMachinesStructuredWithUses() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Marriage.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedInputSpace = new HashSet<String>();
		expectedInputSpace.add("mm");
		expectedInputSpace.add("ff");
		expectedInputSpace.add("marriage");
		expectedInputSpace.add("male");
		expectedInputSpace.add("female");
		
		assertEquals(expectedInputSpace, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetInputSpaceForMachinesStructuredWithExtends() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Registrar.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedInputSapce = new HashSet<String>();
		expectedInputSapce.add("nn");
		expectedInputSapce.add("male");
		expectedInputSapce.add("female");
		expectedInputSapce.add("marriage");
		
		assertEquals(expectedInputSapce, partitioner.getOperationInputSpace());
	}
	
	
	
	@Test
	public void shouldGetOperationCharacteristics() {
		Machine machine = getMachineInstance("machines/Test.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("foo : BOOL");
		expectedCharacteristics.add("pressed : BOOL");
		expectedCharacteristics.add("test_variable <: NAT1");
		expectedCharacteristics.add("test_variable2 <: NAT1");
		expectedCharacteristics.add("test_variable3 <: NAT1");
		expectedCharacteristics.add("((pressed = TRUE) => (foo = FALSE))");
		expectedCharacteristics.add("((test_variable3 = test_variable) => (foo = TRUE))");
		expectedCharacteristics.add("((test_variable2 = test_variable) => (test_variable3 /= test_variable))");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetOperationCharacteristicsWhenItHasConditionals() {
		Machine machine = getMachineInstance("machines/Player.mch");
		Operation operationUnderTest = machine.getOperation(1);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("pp : PLAYER");
		expectedCharacteristics.add("pp : team");
		expectedCharacteristics.add("team <: PLAYER");
		expectedCharacteristics.add("card(team) = 11");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetCharacteristicsForMachineStructuredWithIncludes() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Locks.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("dd : DOOR");
		expectedCharacteristics.add("status(dd) = unlocked");
		expectedCharacteristics.add("status : (DOOR --> STATUS)");
		expectedCharacteristics.add("position~[{open}] <: status~[{unlocked}]");
		expectedCharacteristics.add("position : (DOOR --> POSITION)");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetCharacteristicsFromPromotedOperations() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Locks.mch");
		Operation operationUnderTest = machine.getOperation(3);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("dd : DOOR");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetCharacteristicsForMachineStructuredWithSees() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Costumer.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("gg : GOODS");
		expectedCharacteristics.add("limit : (GOODS --> NAT1)");
		expectedCharacteristics.add("price : (GOODS --> NAT1)");
		expectedCharacteristics.add("price(gg) <= limit(gg)");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetCharacteristicsForMachinesStructuredWithUses() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Marriage.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("mm : male");
		expectedCharacteristics.add("ff : female");
		expectedCharacteristics.add("mm /: dom(marriage)");
		expectedCharacteristics.add("ff /: ran(marriage)");
		expectedCharacteristics.add("marriage : (male >+> female)");
		expectedCharacteristics.add("male <: PERSON");
		expectedCharacteristics.add("female <: PERSON");
		expectedCharacteristics.add("male /\\ female = {}");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetCharacteristicsForMachinesStructuredWithExtends() {
		Machine machine = getMachineInstance("machines/exemplos_schneider/Registrar.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);
		
		Set<String> expectedCharacteristics = new HashSet<String>();
		expectedCharacteristics.add("nn : male \\/ female");
		expectedCharacteristics.add("male <: PERSON");
		expectedCharacteristics.add("female <: PERSON");
		expectedCharacteristics.add("male /\\ female = {}");
		expectedCharacteristics.add("marriage : (male >+> female)");
		expectedCharacteristics.add("nn : dom(marriage)");
		expectedCharacteristics.add("nn : ran(marriage)");
		
		assertEquals(expectedCharacteristics, partitioner.getOperationCharacteristics());
	}
	
	
	
	@Test
	public void shouldGetTypingClauses() {
		Machine machine = getMachineInstance("machines/Test.mch");
		Operation operationUnderTest = machine.getOperation(0);
		Partitioner partitioner = new Partitioner(operationUnderTest);

		Set<String> expectedTypingClauses = new HashSet<String>();
		expectedTypingClauses.add("pressed : BOOL");
		expectedTypingClauses.add("foo : BOOL");
		expectedTypingClauses.add("test_variable <: NAT1");
		expectedTypingClauses.add("test_variable2 <: NAT1");
		expectedTypingClauses.add("test_variable3 <: NAT1");
		
		
		assertEquals(expectedTypingClauses, partitioner.getTypingClauses());
	}
	
	
	
	private Machine getMachineInstance(String path) {
		Machine machine;
		try {
			machine = new Machine(new File(path));
		} catch (BException e) {
			machine = null;
		}
		return machine;
	}
}
